Nuprl Lemma : tl_wf
11,40
postcript
pdf
A
:Type,
l
:(
A
List). tl(
l
)
(
A
List)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
tl(
l
)
origin
A:Type, l:(A List). tl(l) 
(A List) A:Type, l:(A List). tl(l) (A List) Tx:A. B(x)